(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(a(x1)) → b(b(x1))
c(c(b(x1))) → d(c(a(x1)))
a(x1) → d(c(c(x1)))
c(d(x1)) → b(c(x1))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 733
Accept states: [734, 735]
Transitions:
733→734[a_1|0]
733→735[c_1|0]
733→733[b_1|0, d_1|0]
733→736[c_1|1]
733→738[c_1|1]
733→739[a_1|1]
733→741[c_1|2]
736→737[c_1|1]
737→734[d_1|1]
738→735[b_1|1]
738→736[b_1|1]
738→738[b_1|1]
738→741[b_1|1]
738→744[a_1|2]
738→747[c_1|3]
739→740[c_1|1]
740→737[d_1|1]
740→742[d_1|1]
740→746[c_1|2]
740→747[d_1|1]
741→742[c_1|2]
742→739[d_1|2]
742→743[c_1|2]
743→740[b_1|2]
744→745[c_1|2]
745→743[d_1|2]
745→748[d_1|2]
745→750[c_1|3]
746→743[b_1|2]
746→748[b_1|2]
747→748[c_1|3]
748→744[d_1|3]
748→749[c_1|3]
749→745[b_1|3]
750→749[b_1|3]

(2) BOUNDS(O(1), O(n^1))